nontrivial_iff_exists_ne — Mathlib

English

The subtype p is nontrivial iff there exists y ∈ α with p y and y ≠ x, for some x ∈ Subtype p.

Русский

Подтип p тривиален тогда и только тогда, когда существует y ∈ α с p y и y ≠ x, для некоторого x ∈ Subtype p.

LaTeX

$$$$\mathrm{Nontrivial}(\mathrm{Subtype}\,p) \iff \exists y : \alpha, (p\,y) \land y \neq x.$$$$

Lean4

theorem nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) : Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x :=
  by simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

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