max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: protect Equiv

Browse source
This commit is contained in:
François G. Dorais 2021-07-02 06:43:35 -04:00 • committed by Leonardo de Moura
parent d55c069172
commit 1db0bca914
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Core.lean
View file

@ -944,15 +944,15 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)]
namespace Function
variable {α : Sort u} {β : α → Sort v}
def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x
protected def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x
protected theorem Equiv.refl (f : ∀ (x : α), β x) : Equiv f f :=
protected theorem Equiv.refl (f : ∀ (x : α), β x) : Function.Equiv f f :=
fun x => rfl
protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Function.Equiv f₁ f₂ → Function.Equiv f₂ f₁ :=
fun h x => Eq.symm (h x)
protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Function.Equiv f₁ f₂ → Function.Equiv f₂ f₃ → Function.Equiv f₁ f₃ :=
fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x)
protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) := {