inf_eq_inter

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inf_eq_inter

English

For any finite subsets S,T of α, their infimum (meet) with respect to the inclusion order is exactly their intersection: S ⊓ T = S ∩ T.

Русский

Для любых конечных подмножеств S и T множества α их meet по включению равен их пересечению: S ∩ T.

LaTeX

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

Lean4

@[grind =]
theorem inf_eq_inter {s t : Finset α} : s ⊓ t = s ∩ t :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru