comap — Mathlib

English

The mem_comap lemma states the explicit membership equivalence for comap added as a simp lemma.

Русский

Лемма mem_comap сообщает явное эквивалентное членство для comap как simp-лемма.

LaTeX

$$$ \text{@[simp]}\n\theorem mem_comap : s \in comap m g \iff \exists t \in g, m^{-1}'t \subseteq s $$$

Lean4

theorem comap {p : β → Prop} (hf : ∀ᶠ b in g, p b) (f : α → β) : ∀ᶠ a in comap f g, p (f a) :=
  preimage_mem_comap hf

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