biSup_comp — Mathlib

English

For a bijection e : ι ≃ ι' and a set s ⊆ ι', the supremum of g(e i) over i ∈ e^{-1}'' s equals the supremum of g i over i ∈ s.

Русский

Пусть e — биекция и s — подмножество ι'. Тогда супремум g(e(i)) по i∈e^{-1}''s равен супремуму g(i) по i∈s.

LaTeX

$$$ \\bigvee_{i \\in e^{-1}'' s} g(e(i)) = \\bigvee_{i \\in s} g(i). $$$

Lean4

theorem biSup_comp {ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') : ⨆ i ∈ e.symm '' s, g (e i) = ⨆ i ∈ s, g i :=
  by simpa only [iSup_subtype'] using (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

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