infs_subset_iff — Mathlib

English

Let s,t,u be Finsets with infimum operation ⊓. Then s ⊼ t ⊆ u if and only if ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u.

Русский

Пусть s,t,u — конечные множества с операциейInf. Тогда s ⊼ t ⊆ u тогда и только если для всех a∈s и b∈t имеет a ⊓ b ∈ u.

LaTeX

$$$ s \nabla t \subseteq u \iff \forall a \in s, \forall b \in t, a \wedge b \in u $$$

Lean4

@[simp]
theorem infs_subset_iff : s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u :=
  image₂_subset_iff

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