sup_lt_iff — Mathlib

English

In a Boolean algebra, the infimum of f(i) ⇒ a over i ∈ s equals the infimum of f(i) all imply a.

Русский

В булевой алгебре: \bigwedge_{i∈s} (f(i) ⇒ a) = (\bigwedge_{i∈s} f(i)) ⇒ a.

LaTeX

$$$\bigwedge_{b\in s} (f(b) \Rightarrow a) = (\bigwedge_{b\in s} f(b)) \Rightarrow a$$$

Lean4

@[simp]
protected theorem sup_lt_iff (ha : ⊥ < a) : s.sup f < a ↔ ∀ b ∈ s, f b < a :=
  ⟨fun hs _ hb => lt_of_le_of_lt (le_sup hb) hs,
    Finset.cons_induction_on s (fun _ => ha) fun c t hc => by
      simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right⟩

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