toColex_le_toColex — Mathlib

English

For finite s,t ⊆ α, toColex s ≤ toColex t is equivalent to: ∀ a ∈ s, a ∉ t → ∃ b ∈ t ∧ b ∉ s ∧ a ≤ b.

Русский

Для конечных множеств s,t⊆α, toColex s ≤ toColex t эквивалентно: ∀ a ∈ s, a ∉ t → ∃ b ∈ t ∧ b ∉ s ∧ a ≤ b.

LaTeX

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

Lean4

theorem toColex_le_toColex : toColex s ≤ toColex t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t → ∃ b, b ∈ t ∧ b ∉ s ∧ a ≤ b :=
  Iff.rfl

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