mem_infs — Mathlib

English

Membership in the infs set is equivalent to existence of a and b with a ∈ s, b ∈ t and a ⊓ b = c.

Русский

Членство в s ⊼ t эквивалентно существованию a ∈ s и b ∈ t такого, что a ⊓ b = c.

LaTeX

$$$ c \\in s \\tfrac{\\!\\!}{} ⊼ t \\iff \\exists a \\in s, \\exists b \\in t, a \\sqcap b = c $$$

Lean4

@[simp]
theorem mem_infs : c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c := by simp [(· ⊼ ·)]

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