toColex_lt_toColex_iff_exists_forall_lt

English

For α linear, s,t in Colex(Finset α) satisfy s < t iff there exists a ∈ t \\ s with a not in s and every b ∈ s not in t satisfies b < a.

Русский

Для линейного α и элементов s,t в Colex(Finset α) иметь s < t эквивалентно существованию a ∈ t\\s, такого что a не в s, и для каждого b ∈ s\\t, b < a.

LaTeX

$$$$ \\operatorname{toColex}(s) < \\operatorname{toColex}(t) \\iff \\exists a \\in t \\setminus s, a \\notin s \\land \\forall b \\in s, b \\notin t \\rightarrow b < a $$$$

Lean4

theorem toColex_lt_toColex_iff_exists_forall_lt : toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a :=
  by
  rw [← not_le, toColex_le_toColex, not_forall]
  simp only [not_forall, not_exists, not_and, not_le, exists_prop]

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