English
If p is a predicate on α with p(a ⊔ b) ↔ p(a) ∧ p(b) for all a,b, then p(partialSups f i) holds iff p(f(j)) holds for all j ≤ i.
Русский
Пусть p — предикат на α, удовлетворяющий p(a ⊔ b) ⇔ p(a) ∧ p(b). Тогда p(partialSups f i) эквивалентно ∀ j ≤ i, p(f(j)).
LaTeX
$$$p(\\text{partialSups} f \\; i) \\,\\Longleftrightarrow \\, \\forall j \\le i,\\; p(f(j))$$$
Lean4
theorem partialSups_iff_forall {f : ι → α} (p : α → Prop) (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) {i : ι} :
p (partialSups f i) ↔ ∀ j ≤ i, p (f j) := by
classical
rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
· change (Iic i).inf (p ∘ f) ↔ _
simp [Finset.inf_eq_iInf]
· intro x y
rw [hp]
rfl
