mono — Mathlib

English

Under UniqueMul A B a0 b0, the set of pairs (a,b) with a∈A, b∈B and a*b=a0*b0 is a subsingleton.

Русский

При условии UniqueMul A B a0 b0 множество пар (a,b) с a∈A, b∈B и a*b=a0*b0 является пододиночным.

LaTeX

$$$\\text{Set.Subsingleton}\\{(a,b)\\in A\\times B:\\; a b = a_0 b_0\\}$$$

Lean4

@[to_additive]
theorem mono {A' B' : Finset G} (hA : A ⊆ A') (hB : B ⊆ B') (h : UniqueMul A' B' a0 b0) : UniqueMul A B a0 b0 :=
  fun _ _ ha hb he ↦ h (hA ha) (hB hb) he

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