forall_infs_iff — Mathlib

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₂

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