apply_mem_iff

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.IsImage.apply_mem_iff

English

If h: e.IsImage s t, then for any x in the source, e x ∈ t iff x ∈ s.

Русский

Если h: e.IsImage s t, то для любого x из источника, e(x) ∈ t эквивалентно x ∈ s.

LaTeX

$$$\\forall x \\in \\mathrm{source}(e),\\; e(x) \\in t \\iff x \\in s$$$

Lean4

theorem apply_mem_iff (h : e.IsImage s t) (hx : x ∈ e.source) : e x ∈ t ↔ x ∈ s :=
  h hx

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

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

Разделы

Аффилиация

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