toColex_lt_toColex — Mathlib

English

For s,t, we have toColex s < toColex t iff s ≠ t and for all a ∈ s, a ∉ t there exists b ∈ t with b ∉ s and a ≤ b.

Русский

Для s,t выполняется toColex s < toColex t тогда и только тогда, когда s ≠ t и для каждого a∈s, a∉t существует b∈t такой, что b∉s и a ≤ b.

LaTeX

$$$toColex s < toColex t \iff (s \neq t) \land \forall a\ (a \in s \to a \notin t \to \exists b \in t,\; b \notin s \land a \le b)$$$

Lean4

theorem toColex_lt_toColex : toColex s < toColex t ↔ s ≠ t ∧ ∀ ⦃a⦄, a ∈ s → a ∉ t → ∃ b, b ∈ t ∧ b ∉ s ∧ a ≤ b := by
  simp [lt_iff_le_and_ne, toColex_le_toColex, and_comm]

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