Theorems · Theorem · order theory

Set.InjOn.image_iInter_eq

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {f : α → β},
  Set.InjOn f (⋃ i, s i) → f '' ⋂ i, s i = ⋂ i, f '' s i

Defined in

Mathlib.Data.Set.Lattice.Image

Cited by

22 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Nonempty