Theorems · Theorem · order theory

Equiv.iInf_congr

∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι'),
  (∀ (x : ι), g (e x) = f x) → ⨅ x, f x = ⨅ y, g y

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

InfSet