iSup_congr — Mathlib

English

Let f be a surjective function and g : ι' → α. Then ⨆ x, g (f x) = ⨆ y, g y.

Русский

Пусть f — сюръекция, и g : ι' → α. Тогда ⨆ x, g (f x) = ⨆ y, g y.

LaTeX

$$$$ \text{Surjective}(f) \Rightarrow \bigvee_{x} g(f(x)) = \bigvee_{y} g(y) $$$$

Lean4

protected theorem iSup_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) :
    ⨆ x, f x = ⨆ y, g y := by
  convert h1.iSup_comp g
  exact (h2 _).symm

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