mem_map

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.mem_map

English

Membership in a map corresponds to membership in the preimage: t ∈ map m f ⇔ m⁻¹'(t) ∈ f.

Русский

Членство в образе сохраняется через предобраз: t ∈ map m f ⇔ m^{-1}(t) ∈ f.

LaTeX

$$$t \\in map m f \\iff m^{-1}' t \\in f$$$

Lean4

@[simp]
theorem mem_map : t ∈ map m f ↔ m ⁻¹' t ∈ f :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru