card_le_one_iff_subset_singleton — Mathlib

English

If α is nonempty, then #s ≤ 1 iff there exists x ∈ α such that s ⊆ {x}.

Русский

Если тип α непуст, то #s ≤ 1 тогда, когда существует x ∈ α такое, что s ⊆ {x}.

LaTeX

$$[Nonempty α] : #s ≤ 1 ↔ ∃ x : α, s ⊆ { x }$$

Lean4

theorem card_le_one_iff_subset_singleton [Nonempty α] : #s ≤ 1 ↔ ∃ x : α, s ⊆ { x } :=
  by
  refine ⟨fun H => ?_, ?_⟩
  · obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
    · exact ⟨Classical.arbitrary α, empty_subset _⟩
    · exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
  · rintro ⟨x, hx⟩
    rw [← card_singleton x]
    exact card_le_card hx

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