subset_preimage_const — Mathlib

English

Let s be nonempty and c_a be the constant function x ↦ a. Then s ⊆ (c_a)^{-1}(t) iff a ∈ t.

Русский

Пусть s непусто и c_a — константное отображение x ↦ a. Тогда s ⊆ c_a^{-1}(t) тогда и только тогда, когда a ∈ t.

LaTeX

$$$$ s \neq \emptyset \Rightarrow s \subseteq (\mathrm{const}_a)^{-1}(t) \iff a \in t. $$$$

Lean4

@[simp]
theorem subset_preimage_const {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) : s ⊆ (fun _ => a) ⁻¹' t ↔ a ∈ t :=
  by
  rw [← image_subset_iff, hs.image_const, singleton_subset_iff]
    -- Note defeq abuse identifying `preimage` with function composition in the following two proofs.

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