succ_fixpoint_iff — Mathlib

English

For a ChainClosure c, SuccChain r c = c if and only if c = maxChain r; i.e., a chain closure is fixed by succ precisely when it is the maximal chain.

Русский

Для ChainClosure r c succ-цепь равна самому c тогда и только тогда, когда c равно maxChain r; то есть цепочная оболочка фиксируется succ ровно тогда, когда она максимальна.

LaTeX

$$$ (\text{hc} : \ ChainClosure\, r\ c) \to (SuccChain\, r\ c = c) \iff c = maxChain\, r $$$

Lean4

theorem succ_fixpoint_iff (hc : ChainClosure r c) : SuccChain r c = c ↔ c = maxChain r :=
  ⟨fun h => (subset_sUnion_of_mem hc).antisymm <| chainClosure_maxChain.succ_fixpoint hc h, fun h =>
    subset_succChain.antisymm' <| (subset_sUnion_of_mem hc.succ).trans h.symm.subset⟩

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