Theorems · Theorem · order theory

Set.BijOn.iSup_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {s : Set β} {t : Set γ} {f : β → γ}
  (g : γ → α), Set.BijOn f s t → ⨆ x ∈ s, g (f x) = ⨆ y ∈ t, g y

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice