inf_lt_iff

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.inf_lt_iff

English

In a Boolean lattice, for a < ⊤, s.inf f < a iff there exists b ∈ s with f(b) < a.

Русский

В булевой решётке, если a < ⊤, то s.inf f < a ⇔ существует b ∈ s, such что f(b) < a.

LaTeX

$$$a < \top \Rightarrow (s.inf f < a \iff \exists b \in s, f(b) < a)$$$

Lean4

@[simp]
protected theorem inf_lt_iff : s.inf f < a ↔ ∃ b ∈ s, f b < a :=
  @Finset.lt_sup_iff αᵒᵈ _ _ _ _ _ _

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

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

Разделы

Аффилиация

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