nontrivial_of_exists_lt — Mathlib

English

Let α be a preorder and s ⊆ α. If there exist x ∈ s and y ∈ s with x < y, then s is nontrivial (i.e., contains two distinct elements).

Русский

Пусть α — множество с отношением порядка; s ⊆ α. Если существуют x, y ∈ s такие, что x < y, то s не тривиально (содержит два разных элемента).

LaTeX

$$$\big(\exists x \in s, \exists y \in s, x < y\big) \Rightarrow \exists x \in s, \exists y \in s, x \neq y$$$

Lean4

theorem nontrivial_of_exists_lt [Preorder α] (H : ∃ᵉ (x ∈ s) (y ∈ s), x < y) : s.Nontrivial :=
  let ⟨_, hx, _, hy, hxy⟩ := H
  nontrivial_of_lt hx hy hxy

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