pair_subset — Mathlib

English

A set is nontrivial if and only if it contains two distinct elements; equivalently, there exist x,y with x ≠ y and {x,y} ⊆ s.

Русский

Множество не тривиально тогда и только тогда, когда в нем есть два различных элемента; эквивалентно существованию x,y с x ≠ y и {x,y} ⊆ s.

LaTeX

$$$ s.Nontrivial \iff \exists x \exists y, x \neq y \wedge \{x,y\} \subseteq s $$$

Lean4

theorem pair_subset (hs : s.Nontrivial) : ∃ x y, x ≠ y ∧ { x, y } ⊆ s :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, y, hxy, insert_subset hx <| singleton_subset_iff.2 hy⟩

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