English
Let p be a predicate on α. For Finsets s,t ⊆ α with a greatest lower bound operation ⊓, (∀ c ∈ s ⊼ t, p c) holds if and only if ∀ a ∈ s, ∀ b ∈ t, p(a ⊓ b).
Русский
Пусть p — предикат на α. Для конечных множеств s,t с операцией inf ⊓ выполняется (∀ c ∈ s ⊼ t, p c) тогда и только если ∀ a ∈ s, ∀ b ∈ t, p(a ⊓ b).
LaTeX
$$$ (\forall c \in s \nabla t) p(c) \iff \forall a \in s, \forall b \in t, p(a \wedge b) $$$
Lean4
theorem forall_infs_iff {p : α → Prop} : (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b) :=
forall_mem_image₂