nfBelow_iff_topBelow — Mathlib

English

For any b with NF, and any ONote o, NFBelow o (repr b) holds if and only if NF o and TopBelow b o hold.

Русский

Для любого b с NF и любого o, NFBelow o (repr b) эквивалентно тому, что NF o и TopBelow b o.

LaTeX

$$$\forall b : ONote\, [b.NF]\;\forall o : ONote,\; NFBelow\; o\; (repr\; b) \iff (NF\; o) \wedge (TopBelow\; b\; o)$$$

Lean4

theorem nfBelow_iff_topBelow {b} [NF b] : ∀ {o}, NFBelow o (repr b) ↔ NF o ∧ TopBelow b o
  | 0 => ⟨fun h => ⟨⟨⟨_, h⟩⟩, trivial⟩, fun _ => NFBelow.zero⟩
  | oadd _ _ _ =>
    ⟨fun h => ⟨⟨⟨_, h⟩⟩, (@cmp_compares _ b h.fst _).eq_lt.2 h.lt⟩, fun ⟨h₁, h₂⟩ =>
      h₁.below_of_lt <| (@cmp_compares _ b h₁.fst _).eq_lt.1 h₂⟩

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