inf_eq_inter' — Mathlib

English

Let S and T be finite subsets of a type α with decidable equality. The meet (greatest lower bound) of S and T with respect to subset inclusion coincides with their set-theoretic intersection: S ⊓ T = S ∩ T.

Русский

Пусть S и T — конечные подмножества множества α. Их meet по отношению ⊆ равен их пересечению: S ∩ T.

LaTeX

$$$ s \sqcap t = s \cap t $$$

Lean4

@[simp]
theorem inf_eq_inter' : (Min.min : Finset α → Finset α → Finset α) = Inter.inter :=
  rfl

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