lt_rank_iff — Mathlib

English

For any o and x, o < rank x iff there exists y ∈ x with o ≤ rank y.

Русский

Для любого o и x, o < rank(x) тогда и только тогда, существует y ∈ x, такой что o ≤ rank(y).

LaTeX

$$$$ o < \operatorname{rank}(x) \iff \exists y \in x,\; o \le \operatorname{rank}(y) $$$$

Lean4

theorem lt_rank_iff {o : Ordinal} {x : PSet} : o < rank x ↔ ∃ y ∈ x, o ≤ rank y :=
  by
  rw [← not_iff_not, not_lt, rank_le_iff]
  simp

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