preimage_subset

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.preimage_subset

English

For any subsets s,t of β, e^{-1}(s) ⊆ e^{-1}(t) if and only if s ⊆ t.

Русский

Для подмножеств s,t ⊆ β верно: e^{-1}(s) ⊆ e^{-1}(t) тогда и только тогда, когда s ⊆ t.

LaTeX

$$$ e^{-1}(s) \subseteq e^{-1}(t) \iff s \subseteq t $$$

Lean4

theorem preimage_subset {α β} (e : α ≃ β) (s t : Set β) : e ⁻¹' s ⊆ e ⁻¹' t ↔ s ⊆ t :=
  e.surjective.preimage_subset_preimage_iff

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

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

Разделы

Аффилиация

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