one_lt_encard_iff — Mathlib

English

1 < encard(s) if and only if there exist two elements of s that are distinct.

Русский

1 < encard(S) тогда и только тогда существуют два элемента S, которые различны.

LaTeX

$$$1 < encard(s) \\iff \\exists a b, a \\in s \\land b \\in s \\land a \\neq b$$$

Lean4

theorem one_lt_encard_iff : 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b := by
  rw [← not_iff_not, not_exists, not_lt, encard_le_one_iff]; aesop

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