comap_boundedBy — Mathlib

English

For a function f : β → α, the comap of boundedBy m equals boundedBy of m composed with image under f: comap f (boundedBy m) = boundedBy (λ s, m (f '' s)).

Русский

Для функции f : β → α выполняется, что comap f (boundedBy m) = boundedBy (λ s, m (f '' s)).

LaTeX

$$$\\mathrm{comap}_f(\\mathrm{boundedBy}(m)) = \\mathrm{boundedBy}(s \\mapsto m(f'' s))$$$

Lean4

theorem comap_boundedBy {β} (f : β → α) (h : (Monotone fun s : { s : Set α // s.Nonempty } => m s) ∨ Surjective f) :
    comap f (boundedBy m) = boundedBy fun s => m (f '' s) :=
  by
  refine (comap_ofFunction _ ?_).trans ?_
  · refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
    have ht : t.Nonempty := hs.mono hst
    exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)
  · dsimp only [boundedBy]
    congr with s : 1
    rw [image_nonempty]

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