Theorems · Theorem · order theory

Set.preimage_const

∀ {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [inst : Decidable (b ∈ s)],
  (fun x => b) ⁻¹' s = if b ∈ s then Set.univ else ∅

Defined in

Mathlib.Data.Set.Image

Cited by

12 results in Mathlib

Foundations

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

Assumes

Decidable