image_subset_infs_left — Mathlib

English

For any predicate p, (∀ c ∈ s ⊼ t, p c) holds iff ∀ a ∈ s, ∀ b ∈ t, p(a ⊓ b).

Русский

Для любого предиката p выполняется: (∀ c ∈ s ⊼ t, p c) тогда и только тогда, когда ∀ a ∈ s, ∀ b ∈ t, p(a ∧ b).

LaTeX

$$$ (\forall c \in s \⊼ t, p c) \iff (\forall a \in s, \forall b \in t, p(a \wedge b)) $$$

Lean4

theorem image_subset_infs_left : b ∈ t → (fun a => a ⊓ b) '' s ⊆ s ⊼ t :=
  image_subset_image2_left

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