image_const — Mathlib

English

For a nonempty set s and a constant a, the image of s under the constant map to a is {a}.

Русский

Для непустого множества s и константного отображения в a образом s является {a}.

LaTeX

$$$ (\\lambda x. a)'' s = \\{ a \\}, \\quad s \\text{ nonempty}. $$$

Lean4

@[simp]
theorem image_const {s : Set α} (hs : s.Nonempty) (a : β) : (fun _ => a) '' s = { a } :=
  ext fun _ =>
    ⟨fun ⟨_, _, h⟩ => h ▸ mem_singleton _, fun h => (eq_of_mem_singleton h).symm ▸ hs.imp fun _ hy => ⟨hy, rfl⟩⟩

Похожие утверждения