Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
import Mt.Utils.List
import Mt.Utils.Nat
namespace Mt.Utils
theorem forall_ext : ∀ {α : Type } {f g : α → Prop (∀ (a : α ), f a = g a ) → (∀ (a : α ), f a ) = ∀ (a : α ), g a forall_ext { α : Type } { f g : α -> Prop }
( h : ∀ a : α , f a = g a ) : (∀ a : α , f a ) = (∀ a : α , g a ) := by
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a (∀ (a : α ), f a ) = ∀ (a : α ), g a apply propext : ∀ {a b : Prop }, (a ↔ b a = b α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a (∀ (a : α ), f a ) ↔ ∀ (a : α ), g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a (∀ (a : α ), f a ) = ∀ (a : α ), g a constructor α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a.mp (∀ (a : α ), f a ) → ∀ (a : α ), g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a.mpr (∀ (a : α ), g a ) → ∀ (a : α ), f a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a (∀ (a : α ), f a ) ↔ ∀ (a : α ), g a <;> α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a.mp (∀ (a : α ), f a ) → ∀ (a : α ), g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a.mpr (∀ (a : α ), g a ) → ∀ (a : α ), f a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a a (∀ (a : α ), f a ) ↔ ∀ (a : α ), g a intro h' a α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), f a a : α a.mp g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a (∀ (a : α ), f a ) = ∀ (a : α ), g a . α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), f a a : α a.mp g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), f a a : α a.mp g a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), g a a : α a.mpr f a
exact Eq.mp : ∀ {α β : Sort ?u.69 }, α = β α → β ( h a ) ( h' a )
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a (∀ (a : α ), f a ) = ∀ (a : α ), g a . α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), g a a : α a.mpr f a
α : Type f, g : α → Prop h : ∀ (a : α ), f a = g a h' : ∀ (a : α ), g a a : α a.mpr f a
exact Eq.mpr : ∀ {α β : Sort ?u.72 }, α = β β → α ( h a ) ( h' a )
end Mt.Utils