Theorems · Theorem · order theory

Set.InjOn.image_biInter_eq

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {p : ι → Prop} {s : (i : ι) → p i → Set α},
  (∃ i, p i) →
    ∀ {f : α → β},
      Set.InjOn f (⋃ i, ⋃ (hi : p i), s i hi) → f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Defined in

Mathlib.Data.Set.Lattice.Image

Cited by

1 results in Mathlib

Foundations

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