chore: use the same names as in mathport (#200)

Ideally this would cause mathport to align these definitions, and then we can translate the notation.

Author: gebner

Mathlib/Data/Equiv/Basic.lean

@@ -23,8 +23,8 @@ variable {α : Sort u} {β : Sort v} {γ : Sort w}
 structure Equiv (α : Sort u) (β : Sort v) where
   toFun    : α → β
   invFun   : β → α
-  leftInv  : left_inverse invFun toFun
-  rightInv : right_inverse invFun toFun
+  left_inv  : LeftInverse invFun toFun
+  right_inv : RightInverse invFun toFun
 
 infix:25 " ≃ " => Equiv
 
@@ -45,22 +45,22 @@ def refl (α) : α ≃ α := ⟨id, id, λ _ => rfl, λ _ => rfl⟩
 
 instance : Inhabited (α ≃ α) := ⟨Equiv.refl α⟩
 
-def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.rightInv, e.leftInv⟩
+def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.right_inv, e.left_inv⟩
 
 
 def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β),
-  e₂.leftInv.comp e₁.leftInv, e₂.rightInv.comp e₁.rightInv⟩
+  e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
 
 theorem to_fun_as_coe (e : α ≃ β) : e.toFun = e := rfl
 
 @[simp] theorem inv_fun_as_coe (e : α ≃ β) : e.invFun = e.symm := rfl
 
 @[simp] theorem apply_symm_apply  (e : α ≃ β) (x : β) : e (e.symm x) = x :=
-e.rightInv x
+e.right_inv x
 
 @[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x :=
-e.leftInv x
+e.left_inv x
 
 @[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ (e : α → β) = id := funext e.symm_apply_apply
 

Mathlib/Data/Equiv/Functor.lean

@@ -31,8 +31,8 @@ theorem map_map (m : α → β) (g : β → γ) (x : f α) :
 def map_equiv (h : α ≃ β) : f α ≃ f β where
   toFun    := map h
   invFun   := map h.symm
-  leftInv x := by simp [map_map]
-  rightInv x := by simp [map_map]
+  left_inv x := by simp [map_map]
+  right_inv x := by simp [map_map]
 
 @[simp]
 lemma map_equiv_apply (h : α ≃ β) (x : f α) :

Mathlib/Data/Prod.lean

@@ -121,17 +121,17 @@ def swap : α × β → β × α := λp => (p.2, p.1)
 @[simp] lemma swap_swap_eq : swap ∘ swap = @id (α × β) :=
 funext swap_swap
 
-lemma swap_left_inverse : Function.left_inverse (@swap α β) swap :=
+lemma swap_LeftInverse : Function.LeftInverse (@swap α β) swap :=
 swap_swap
 
-lemma swap_right_inverse : Function.right_inverse (@swap α β) swap :=
+lemma swap_RightInverse : Function.RightInverse (@swap α β) swap :=
 swap_swap
 
 lemma swap_injective : Function.injective (@swap α β) :=
-swap_left_inverse.injective
+swap_LeftInverse.injective
 
 lemma swap_surjective : Function.surjective (@swap α β) :=
-Function.right_inverse.surjective swap_left_inverse
+Function.RightInverse.surjective swap_LeftInverse
 
 lemma swap_bijective : Function.bijective (@swap α β) :=
 ⟨swap_injective, swap_surjective⟩

Mathlib/Init/Function.lean

@@ -69,37 +69,37 @@ def bijective (f : α → β) := injective f ∧ surjective f
 theorem bijective.comp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)
 | ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩
 
-/-- `left_inverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
-def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
+/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
+def LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
 
-/-- `has_left_inverse f` means that `f` has an unspecified left inverse. -/
-def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f
+/-- `has_LeftInverse f` means that `f` has an unspecified left inverse. -/
+def has_LeftInverse (f : α → β) : Prop := ∃ finv : β → α, LeftInverse finv f
 
-/-- `right_inverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
-def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
+/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
+def RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g
 
-/-- `has_right_inverse f` means that `f` has an unspecified right inverse. -/
-def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f
+/-- `has_RightInverse f` means that `f` has an unspecified right inverse. -/
+def has_RightInverse (f : α → β) : Prop := ∃ finv : β → α, RightInverse finv f
 
-theorem left_inverse.injective {g : β → α} {f : α → β} : left_inverse g f → injective f :=
+theorem LeftInverse.injective {g : β → α} {f : α → β} : LeftInverse g f → injective f :=
 λ h a b hf => h a ▸ h b ▸ hf ▸ rfl
 
-theorem has_left_inverse.injective {f : α → β} : has_left_inverse f → injective f :=
+theorem has_LeftInverse.injective {f : α → β} : has_LeftInverse f → injective f :=
 λ h => Exists.elim h (λ finv inv => inv.injective)
 
-theorem right_inverse_of_injective_of_left_inverse {f : α → β} {g : β → α}
-    (injf : injective f) (lfg : left_inverse f g) :
-  right_inverse f g :=
+theorem RightInverse_of_injective_of_LeftInverse {f : α → β} {g : β → α}
+    (injf : injective f) (lfg : LeftInverse f g) :
+  RightInverse f g :=
 λ x => injf $ lfg $ f x
 
-theorem right_inverse.surjective {f : α → β} {g : β → α} (h : right_inverse g f) : surjective f :=
+theorem RightInverse.surjective {f : α → β} {g : β → α} (h : RightInverse g f) : surjective f :=
 λ y => ⟨g y, h y⟩
 
-theorem has_right_inverse.surjective {f : α → β} : has_right_inverse f → surjective f
+theorem has_RightInverse.surjective {f : α → β} : has_RightInverse f → surjective f
 | ⟨finv, inv⟩ => inv.surjective
 
-theorem left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α} (surjf : surjective f)
-  (rfg : right_inverse f g) : left_inverse f g :=
+theorem LeftInverse_of_surjective_of_RightInverse {f : α → β} {g : β → α} (surjf : surjective f)
+  (rfg : RightInverse f g) : LeftInverse f g :=
 λ y =>
   let ⟨x, hx⟩ := surjf y
   by rw [← hx, rfg]
@@ -130,10 +130,10 @@ rfl
 @[simp] theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
 funext (λ ⟨a, b⟩ => rfl)
 
-protected theorem left_inverse.id {g : β → α} {f : α → β} (h : left_inverse g f) : g ∘ f = id :=
+protected theorem LeftInverse.id {g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id :=
 funext h
 
-protected theorem right_inverse.id {g : β → α} {f : α → β} (h : right_inverse g f) : f ∘ g = id :=
+protected theorem RightInverse.id {g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id :=
 funext h
 
 end Function

Mathlib/Init/Logic.lean

@@ -561,7 +561,7 @@ def commutative        := ∀ a b, f a b = f b a
 def associative        := ∀ a b c, f (f a b) c = f a (f b c)
 def left_identity      := ∀ a, f one a = a
 def right_identity     := ∀ a, f a one = a
-def right_inverse      := ∀ a, f a (inv a) = one
+def RightInverse      := ∀ a, f a (inv a) = one
 def left_cancelative   := ∀ a b c, f a b = f a c → b = c
 def right_cancelative  := ∀ a b c, f a b = f c b → a = c
 def left_distributive  := ∀ a b c, f a (g b c) = g (f a b) (f a c)

Mathlib/Logic/Function/Basic.lean

@@ -191,7 +191,7 @@ theorem cantor_surjective {α} (f : α → Set α) : ¬ Function.surjective f
 theorem cantor_injective {α : Type _} (f : (Set α) → α) :
   ¬ Function.injective f
 | i => cantor_surjective (λ a b => ∀ U, a = f U → U b) $
-       right_inverse.surjective
+       RightInverse.surjective
          (λ U => funext $ λ a => propext ⟨λ h => h U rfl, λ h' U' e => i e ▸ h'⟩)
 
 /-- `g` is a partial inverse to `f` (an injective but not necessarily
@@ -211,42 +211,42 @@ theorem injective_of_partial_inv_right {α β} {f : α → β} {g} (H : is_parti
  (x y b) (h₁ : g x = some b) (h₂ : g y = some b) : x = y :=
 ((H _ _).1 h₁).symm.trans ((H _ _).1 h₂)
 
-theorem left_inverse.comp_eq_id {f : α → β} {g : β → α} (h : left_inverse f g) : f ∘ g = id :=
+theorem LeftInverse.comp_eq_id {f : α → β} {g : β → α} (h : LeftInverse f g) : f ∘ g = id :=
 funext h
 
-theorem left_inverse_iff_comp {f : α → β} {g : β → α} : left_inverse f g ↔ f ∘ g = id :=
-⟨left_inverse.comp_eq_id, congr_fun⟩
+theorem LeftInverse_iff_comp {f : α → β} {g : β → α} : LeftInverse f g ↔ f ∘ g = id :=
+⟨LeftInverse.comp_eq_id, congr_fun⟩
 
-theorem right_inverse.comp_eq_id {f : α → β} {g : β → α} (h : right_inverse f g) : g ∘ f = id :=
+theorem RightInverse.comp_eq_id {f : α → β} {g : β → α} (h : RightInverse f g) : g ∘ f = id :=
 funext h
 
-theorem right_inverse_iff_comp {f : α → β} {g : β → α} : right_inverse f g ↔ g ∘ f = id :=
-⟨right_inverse.comp_eq_id, congr_fun⟩
+theorem RightInverse_iff_comp {f : α → β} {g : β → α} : RightInverse f g ↔ g ∘ f = id :=
+⟨RightInverse.comp_eq_id, congr_fun⟩
 
-theorem left_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
-  (hf : left_inverse f g) (hh : left_inverse h i) : left_inverse (h ∘ f) (g ∘ i) :=
+theorem LeftInverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+  (hf : LeftInverse f g) (hh : LeftInverse h i) : LeftInverse (h ∘ f) (g ∘ i) :=
 λ a => show h (f (g (i a))) = a by rw [hf (i a), hh a]
 
-theorem right_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
-  (hf : right_inverse f g) (hh : right_inverse h i) : right_inverse (h ∘ f) (g ∘ i) :=
-left_inverse.comp hh hf
+theorem RightInverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+  (hf : RightInverse f g) (hh : RightInverse h i) : RightInverse (h ∘ f) (g ∘ i) :=
+LeftInverse.comp hh hf
 
-theorem left_inverse.right_inverse {f : α → β} {g : β → α} (h : left_inverse g f) :
-  right_inverse f g := h
+theorem LeftInverse.RightInverse {f : α → β} {g : β → α} (h : LeftInverse g f) :
+  RightInverse f g := h
 
-theorem right_inverse.left_inverse {f : α → β} {g : β → α} (h : right_inverse g f) :
-  left_inverse f g := h
+theorem RightInverse.LeftInverse {f : α → β} {g : β → α} (h : RightInverse g f) :
+  LeftInverse f g := h
 
-theorem left_inverse.surjective {f : α → β} {g : β → α} (h : left_inverse f g) :
+theorem LeftInverse.surjective {f : α → β} {g : β → α} (h : LeftInverse f g) :
   surjective f :=
-h.right_inverse.surjective
+h.RightInverse.surjective
 
-theorem right_inverse.injective {f : α → β} {g : β → α} (h : right_inverse f g) :
+theorem RightInverse.injective {f : α → β} {g : β → α} (h : RightInverse f g) :
   injective f :=
-h.left_inverse.injective
+h.LeftInverse.injective
 
-theorem left_inverse.eq_right_inverse {f : α → β} {g₁ g₂ : β → α} (h₁ : left_inverse g₁ f)
-  (h₂ : Function.right_inverse g₂ f) :
+theorem LeftInverse.eq_RightInverse {f : α → β} {g₁ g₂ : β → α} (h₁ : LeftInverse g₁ f)
+  (h₂ : Function.RightInverse g₂ f) :
   g₁ = g₂ := by
   have h₃ : g₁ = g₁ ∘ f ∘ g₂ := by rw [h₂.comp_eq_id, comp.right_id]
   have h₄ : g₁ ∘ f ∘ g₂ = g₂ := by rw [← comp.assoc, h₁.comp_eq_id, comp.left_id]
@@ -318,33 +318,33 @@ inv_fun_on_eq $ let ⟨a, ha⟩ := h
 lemma inv_fun_neg (h : ¬ ∃ a, f a = b) : inv_fun f b = Classical.choice n :=
 by refine inv_fun_on_neg (mt ?_ h); exact λ ⟨a, _, ha⟩ => ⟨a, ha⟩
 
-theorem inv_fun_eq_of_injective_of_right_inverse {g : β → α}
-  (hf : injective f) (hg : right_inverse g f) : inv_fun f = g :=
+theorem inv_fun_eq_of_injective_of_RightInverse {g : β → α}
+  (hf : injective f) (hg : RightInverse g f) : inv_fun f = g :=
 funext $ λ b => hf (by rw [hg b]
                        exact inv_fun_eq ⟨g b, hg b⟩)
 
-lemma right_inverse_inv_fun (hf : surjective f) : right_inverse (inv_fun f) f :=
+lemma RightInverse_inv_fun (hf : surjective f) : RightInverse (inv_fun f) f :=
 λ b => inv_fun_eq $ hf b
 
-lemma left_inverse_inv_fun (hf : injective f) : left_inverse (inv_fun f) f :=
+lemma LeftInverse_inv_fun (hf : injective f) : LeftInverse (inv_fun f) f :=
 λ b => have : f (inv_fun f (f b)) = f b := inv_fun_eq ⟨b, rfl⟩
        hf this
 
 lemma inv_fun_surjective (hf : injective f) : surjective (inv_fun f) :=
-(left_inverse_inv_fun hf).surjective
+(LeftInverse_inv_fun hf).surjective
 
-lemma inv_fun_comp (hf : injective f) : inv_fun f ∘ f = id := funext $ left_inverse_inv_fun hf
+lemma inv_fun_comp (hf : injective f) : inv_fun f ∘ f = id := funext $ LeftInverse_inv_fun hf
 
 end inv_fun
 
 section inv_fun
 variable {α : Type u} [i : Nonempty α] {β : Sort v} {f : α → β}
 
-lemma injective.has_left_inverse (hf : injective f) : has_left_inverse f :=
-⟨inv_fun f, left_inverse_inv_fun hf⟩
+lemma injective.has_LeftInverse (hf : injective f) : has_LeftInverse f :=
+⟨inv_fun f, LeftInverse_inv_fun hf⟩
 
-lemma injective_iff_has_left_inverse : injective f ↔ has_left_inverse f :=
-⟨injective.has_left_inverse, has_left_inverse.injective⟩
+lemma injective_iff_has_LeftInverse : injective f ↔ has_LeftInverse f :=
+⟨injective.has_LeftInverse, has_LeftInverse.injective⟩
 
 end inv_fun
 
@@ -357,24 +357,24 @@ noncomputable def surj_inv {f : α → β} (h : surjective f) (b : β) : α := C
 
 lemma surj_inv_eq (h : surjective f) (b) : f (surj_inv h b) = b := Classical.choose_spec (h b)
 
-lemma right_inverse_surj_inv (hf : surjective f) : right_inverse (surj_inv hf) f :=
+lemma RightInverse_surj_inv (hf : surjective f) : RightInverse (surj_inv hf) f :=
 surj_inv_eq hf
 
-lemma left_inverse_surj_inv (hf : bijective f) : left_inverse (surj_inv hf.2) f :=
-right_inverse_of_injective_of_left_inverse hf.1 (right_inverse_surj_inv hf.2)
+lemma LeftInverse_surj_inv (hf : bijective f) : LeftInverse (surj_inv hf.2) f :=
+RightInverse_of_injective_of_LeftInverse hf.1 (RightInverse_surj_inv hf.2)
 
-lemma surjective.has_right_inverse (hf : surjective f) : has_right_inverse f :=
-⟨_, right_inverse_surj_inv hf⟩
+lemma surjective.has_RightInverse (hf : surjective f) : has_RightInverse f :=
+⟨_, RightInverse_surj_inv hf⟩
 
-lemma surjective_iff_has_right_inverse : surjective f ↔ has_right_inverse f :=
-⟨surjective.has_right_inverse, has_right_inverse.surjective⟩
+lemma surjective_iff_has_RightInverse : surjective f ↔ has_RightInverse f :=
+⟨surjective.has_RightInverse, has_RightInverse.surjective⟩
 
-lemma bijective_iff_has_inverse : bijective f ↔ ∃ g, left_inverse g f ∧ right_inverse g f :=
-⟨λ hf =>  ⟨_, left_inverse_surj_inv hf, right_inverse_surj_inv hf.2⟩,
+lemma bijective_iff_has_inverse : bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f :=
+⟨λ hf =>  ⟨_, LeftInverse_surj_inv hf, RightInverse_surj_inv hf.2⟩,
  λ ⟨g, gl, gr⟩ => ⟨gl.injective,  gr.surjective⟩⟩
 
 lemma injective_surj_inv (h : surjective f) : injective (surj_inv h) :=
-(right_inverse_surj_inv h).injective
+(RightInverse_surj_inv h).injective
 
 lemma surjective_to_subsingleton [na : Nonempty α] [Subsingleton β] (f : α → β) :
   surjective f :=
@@ -564,21 +564,20 @@ end bicomp
 
 section uncurry
 
-variable {α β γ δ : Type _}
-
 /-- Records a way to turn an element of `α` into a function from `β` to `γ`. The most generic use
 is to recursively uncurry. For instance `f : α → β → γ → δ` will be turned into
 `↿f : α × β × γ → δ`. One can also add instances for bundled maps. -/
-class has_uncurry (α : Type _) (β : outParam (Type _)) (γ : outParam (Type _)) := (uncurry : α → (β → γ))
+class HasUncurry (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  uncurry : α → (β → γ)
 
 /- Uncurrying operator. The most generic use is to recursively uncurry. For instance
 `f : α → β → γ → δ` will be turned into `↿f : α × β × γ → δ`. One can also add instances
 for bundled maps. -/
-notation:max "↿" x:max => has_uncurry.uncurry x
+notation:max "↿" x:max => HasUncurry.uncurry x
 
-instance has_uncurry_base : has_uncurry (α → β) α β := ⟨id⟩
+instance HasUncurry_base : HasUncurry (α → β) α β := ⟨id⟩
 
-instance has_uncurry_induction [has_uncurry β γ δ] : has_uncurry (α → β) (α × γ) δ :=
+instance HasUncurry_induction [HasUncurry β γ δ] : HasUncurry (α → β) (α × γ) δ :=
 ⟨λ f p => ↿(f p.1) p.2⟩
 
 end uncurry
@@ -595,10 +594,10 @@ variable {α : Sort u} {f : α → α} (h : involutive f)
 @[simp]
 lemma comp_self : f ∘ f = id := funext h
 
-protected lemma left_inverse : left_inverse f f := h
-protected lemma right_inverse : right_inverse f f := h
+protected lemma LeftInverse : LeftInverse f f := h
+protected lemma RightInverse : RightInverse f f := h
 
-protected lemma injective : injective f := h.left_inverse.injective
+protected lemma injective : injective f := h.LeftInverse.injective
 protected lemma surjective : surjective f := λ x => ⟨f x, h x⟩
 protected lemma bijective : bijective f := ⟨h.injective, h.surjective⟩