apply_mem_map_iff

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.apply_mem_map_iff

English

If f is injective, then f a ∈ L.map f iff a ∈ L.

Русский

Если f инъективно, то f(a) ∈ L.map f тогда и только тогда, когда a ∈ L.

LaTeX

$$$\text{Injective } f \Rightarrow (f(a) \in L.map f \iff a \in L)$$$

Lean4

theorem apply_mem_map_iff (hf : Injective f) : f a ∈ L.map f ↔ a ∈ L :=
  hf.mem_set_image

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

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

Разделы

Аффилиация

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