fundamentalSequenceProp_inl_some — Mathlib

English

FundamentalSequenceProp applied to Sum.inl (some a) holds if and only if repr o equals succ a.repr and (o.NF → a.NF).

Русский

FundamentalSequenceProp для Sum.inl (some a) эквивалентно repr(o) = succ(a.repr) и (o.NF → a.NF).

LaTeX

$$$\\text{FundamentalSequenceProp}(o)(\\text{Sum.inl (some a)}) \\iff o.repr = \\operatorname{succ}(a.repr) \\land (o.NF \\rightarrow a.NF)$$$

Lean4

theorem fundamentalSequenceProp_inl_some (o a) :
    FundamentalSequenceProp o (Sum.inl (some a)) ↔ o.repr = succ a.repr ∧ (o.NF → a.NF) :=
  Iff.rfl

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