invVeblen₁_lt_iff — Mathlib

English

The strict inequality invVeblen₁(o) < o holds exactly when o ≠ 0 and o ∉ range Γ_.

Русский

Строгое неравенство invVeblen₁(o) < o выполняется тогда, когда o ≠ 0 и o не принадлежит диапазону Γ_.

LaTeX

$$$$ invVeblen₁(o) < o \iff o \neq 0 \land o \notin \operatorname{range}(\Gamma_). $$$$

Lean4

theorem invVeblen₁_lt_iff : invVeblen₁ o < o ↔ o ≠ 0 ∧ o ∉ range Γ_ := by
  rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]

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