toColex_le_singleton — Mathlib

English

If s is a strict subset of t, then in Colex, s is strictly less than t.

Русский

Если s является строгим подмножеством t, то в Colex s строго меньше t.

LaTeX

$$$s \subset t \Rightarrow toColex s < toColex t$$$

Lean4

/-- `s ≤ {a}` in colex iff all elements of `s` are strictly less than `a`, except possibly `a` in
which case `s = {a}`. -/
theorem toColex_le_singleton : toColex s ≤ toColex { a } ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a) :=
  by
  simp only [toColex_le_toColex, mem_singleton, exists_eq_left]
  refine forall₂_congr fun b _ ↦ ?_; obtain rfl | hba := eq_or_ne b a <;> aesop

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