eq_of_forall_subset_iff

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.eq_of_forall_subset_iff

English

If for all U, S ⊆ U iff T ⊆ U, then S = T.

Русский

Если для всех U выполняется S ⊆ U ⇔ T ⊆ U, то S = T.

LaTeX

$$$\\forall U\\subseteq\\alpha, (S\\subseteq U) \\Leftrightarrow (T\\subseteq U) \\Rightarrow S=T$$$

Lean4

theorem eq_of_forall_subset_iff (h : ∀ u, s ⊆ u ↔ t ⊆ u) : s = t :=
  eq_of_forall_ge_iff h

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

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

Разделы

Аффилиация

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