fix_fwd — Mathlib

English

If b is in f.fix(a) and a' is the forward step from a (Sum.inr(a') ∈ f(a)), then b is in f.fix(a').

Русский

Если b принадлежит f.fix(a) и a' является прямым переходом из a (Sum.inr(a') ∈ f(a)), то b ∈ f.fix(a').

LaTeX

$$$\\forall f:\\,\\alpha \\to. (\\beta \\oplus \\alpha),\\; b:\\beta,\\; a,a' : \\alpha,\\; (b \\in f.fix(a)) \\rightarrow (\\mathrm{inr}(a') \\in f(a)) \\rightarrow b \\in f.fix(a')$$$

Lean4

theorem fix_fwd {f : α →. β ⊕ α} {b : β} {a a' : α} (hb : b ∈ f.fix a) (ha' : Sum.inr a' ∈ f a) : b ∈ f.fix a' := by
  rwa [← fix_fwd_eq ha']

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