iSup_comp — Mathlib

English

Let f : ι → ι' be a surjective function. For any g : ι' → α, ⨆ 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

theorem iSup_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) : ⨆ x, g (f x) = ⨆ y, g y :=
  by
  simp only [iSup.eq_1]
  congr
  exact hf.range_comp g

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