apply_mem_map_iff

Mathlib.Order.Sublattice

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

English

If f is injective, then a ∈ L.map f if and only if f(a) ∈ L.

Русский

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

LaTeX

$$(Iff) (f a) ∈ L ⇔ a ∈ L, при Injective f$$

Lean4

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

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

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

Разделы

Аффилиация

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