of_card_le_one — Mathlib

English

If A,B are finite nonempty sets with |A| ≤ 1 and |B| ≤ 1, then there exists a ∈ A, b ∈ B such that UniqueMul A B a b.

Русский

Если A,B конечны и непусты и имеют размер не более 1, то существует a ∈ A и b ∈ B такой, что UniqueMul A B a b.

LaTeX

$$$\\exists a \\in A,\\; \\exists b \\in B,\\; UniqueMul A B a b$$$

Lean4

@[to_additive of_card_le_one]
theorem of_card_le_one (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : #A ≤ 1) (hB1 : #B ≤ 1) :
    ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b :=
  by
  rw [Finset.card_le_one_iff] at hA1 hB1
  obtain ⟨a, ha⟩ := hA; obtain ⟨b, hb⟩ := hB
  exact ⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩

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