inter_subset

Mathlib.Order.BooleanAlgebra.Set

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

English

a ∩ b ⊆ c iff a ⊆ bᶜ ∪ c.

Русский

a ∩ b ⊆ c эквивалентно a ⊆ bᶜ ∪ c.

LaTeX

$$$a \cap b \subseteq c \iff a \subseteq b^{c} \cup c$$$

Lean4

theorem inter_subset (a b c : Set α) : a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c :=
  forall_congr' fun _ => and_imp.trans <| imp_congr_right fun _ => imp_iff_not_or

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

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

Разделы

Аффилиация

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