inter_of_left

Mathlib.Order.Bounds.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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