finset_inf_le

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#InfPrime.finset_inf_le

English

For InfPrime a, s.inf f ≤ a iff there exists i ∈ s with f i ≤ a.

Русский

Для InfPrime a, s.inf f ≤ a тогда и только тогда, когда существует i ∈ s такое, что f i ≤ a.

LaTeX

$$InfPrime\ a \rightarrow (s.inf f \le a) \leftrightarrow (\exists i ∈ s, f i \le a)$$

Lean4

theorem finset_inf_le (ha : InfPrime a) : s.inf f ≤ a ↔ ∃ i ∈ s, f i ≤ a :=
  @SupPrime.le_finset_sup _ αᵒᵈ _ _ _ _ _ ha

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

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

Разделы

Аффилиация

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