nontrivial_iff_pair_subset — Mathlib

English

Theorem: A set is nontrivial iff there exists a pair x ≠ y with {x,y} ⊆ s.

Русский

Теорема: множество не тривиально тогда и только тогда, когда существует пара x ≠ y такая что {x,y} ⊆ s.

LaTeX

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

Lean4

theorem nontrivial_iff_pair_subset : s.Nontrivial ↔ ∃ x y, x ≠ y ∧ { x, y } ⊆ s :=
  ⟨Nontrivial.pair_subset, fun H =>
    let ⟨_, _, hxy, h⟩ := H
    nontrivial_of_pair_subset hxy h⟩

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