mem_map_equiv

Mathlib.Order.BooleanSubalgebra

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

English

If f is an order isomorphism α ≃o β, then a ∈ L.map f iff f^{-1}(a) ∈ L.

Русский

Если f — тождественное отображение порядка α ≃o β, то a ∈ L.map f эквивалентно f^{-1}(a) ∈ L.

LaTeX

$$$a \in L.map f \iff f^{-1}(a) \in L$$$

Lean4

theorem mem_map_equiv {f : α ≃o β} {a : β} : a ∈ L.map f ↔ f.symm a ∈ L :=
  Set.mem_image_equiv

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

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

Разделы

Аффилиация

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