inter_of_right

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#BddBelow.inter_of_right

English

If t is bounded below, then s ∩ t is bounded below.

Русский

Если t ограничено снизу, то s ∩ t ограничено снизу.

LaTeX

$$$BddBelow(t) \\rightarrow BddBelow(s \\cap t)$$$

Lean4

/-- If `t` is bounded, then so is `s ∩ t` -/
theorem inter_of_right (h : BddBelow t) : BddBelow (s ∩ t) :=
  h.mono inter_subset_right

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

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

Разделы

Аффилиация

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