one_lt_card_iff

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.one_lt_card_iff

English

There are two distinct elements in s iff 1 < |s|.

Русский

Есть два различных элемента в s тогда и только тогда, когда 1 < |s|.

LaTeX

$$$1 < |s| \\iff \\exists a,b \\in s, a \\neq b$$$

Lean4

theorem one_lt_card_iff : 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
  by
  rw [one_lt_card]
  simp only [exists_and_left]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru