English
In a Boolean algebra, for a nonempty finite s, the infimum over i ∈ s of f(i) \ a equals (inf over i ∈ s of f(i)) \ a.
Русский
В булевой алгебре: \bigwedge_{i∈s} (f(i) \ a) = (\bigwedge_{i∈s} f(i)) \ a.
LaTeX
$$$\bigwedge_{b\in s} (f(b) \setminus a) = (\bigwedge_{b\in s} f(b)) \setminus a$$$
Lean4
@[simp]
protected theorem lt_sup_iff : a < s.sup f ↔ ∃ b ∈ s, a < f b :=
by
apply Iff.intro
·
induction s using cons_induction with
| empty => exact (absurd · not_lt_bot)
| cons c t hc ih =>
rw [sup_cons, lt_sup_iff]
exact fun
| Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
| Or.inr h =>
let ⟨b, hb, hlt⟩ := ih h;
⟨b, mem_cons.2 (Or.inr hb), hlt⟩
· exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)
