inter_right

Mathlib.Analysis.Convex.Exposed

URI: https://scilib.ai/kg/mathlib#IsExposed.inter_right

English

If B is exposed to C and C ⊆ A, then A ∩ B is exposed to C.

Русский

Если B экспонировано относительно C и C ⊆ A, то A ∩ B экспонировано относительно C.

LaTeX

$$$$ (IsExposed\ 𝕜\ B\ C) \to (C \subseteq A) \to IsExposed\ 𝕜\ (A \cap B)\ C. $$$$

Lean4

theorem inter_right (hC : IsExposed 𝕜 B C) (hCA : C ⊆ A) : IsExposed 𝕜 (A ∩ B) C :=
  by
  rw [inter_comm]
  exact hC.inter_left hCA

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

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

Разделы

Аффилиация

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