Theorems · Theorem · order theory

Function.Surjective.iSup_congr

∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι'),
  Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⨆ x, f x = ⨆ y, g y

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

14 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext, Quot.sound

Assumes

SupSet