Theorems · Theorem · order theory

Function.Surjective.iInf_congr

∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {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

11 results in Mathlib

Foundations

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

Assumes

InfSet