card_le_one_iff_eq_bot — Mathlib

English

For any submonoid S, card S ≤ 1 iff S = ⊥.

Русский

Для любого подмоноида S верно: card S ≤ 1 тогда и только тогда, когда S = ⊥.

LaTeX

$$$\\\\operatorname{card}(S) \\\\le 1 \\\\iff S = \\\\bot$$$

Lean4

@[to_additive card_le_one_iff_eq_bot]
theorem card_le_one_iff_eq_bot : card S ≤ 1 ↔ S = ⊥ :=
  ⟨fun h => (eq_bot_iff_forall _).2 fun x hx => by simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1, fun h =>
    by simp [h]⟩

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