mem_comap' — Mathlib

English

For s ⊆ α, s ∈ comap f l if and only if the set {y | ∀ x, f x = y → x ∈ s} belongs to l.

Русский

Для подмножества s ⊆ α верно: s ∈ comap f l тогда, когда множество {y | ∀ x, f x = y → x ∈ s} принадлежит l.

LaTeX

$$s ∈ comap f l ↔ {y | ∀ ⦃x⦄, f x = y → x ∈ s} ∈ l$$

Lean4

theorem mem_comap' : s ∈ comap f l ↔ {y | ∀ ⦃x⦄, f x = y → x ∈ s} ∈ l :=
  ⟨fun ⟨t, ht, hts⟩ => mem_of_superset ht fun y hy x hx => hts <| mem_preimage.2 <| by rwa [hx], fun h =>
    ⟨_, h, fun _ hx => hx rfl⟩⟩
    -- TODO: it would be nice to use `kernImage` much more to take advantage of common name and API,
    -- and then this would become `mem_comap'`

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