mkUnder_ext — Mathlib

English

Two arrows f,g: mkUnder R A ⟶ B are equal iff their right components agree on every a ∈ A.

Русский

Две стрелки f,g: mkUnder R A ⟶ B равны тогда и только тогда, когда их правые компоненты совпадают на каждом a ∈ A.

LaTeX

$$$\forall a:\!A,\ f.right(a)=g.right(a) \Rightarrow f=g$$$

Lean4

@[ext]
theorem mkUnder_ext {A : Type u} [CommRing A] [Algebra R A] {B : Under R} {f g : mkUnder R A ⟶ B}
    (h : ∀ a : A, f.right a = g.right a) : f = g := by
  ext x
  exact h x

Похожие утверждения