infClosed

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.infClosed

English

The carrier of a Sublocale is closed under binary infimum: if a and b belong to S, then a ⊓ b belongs to S.

Русский

Носитель подлокали замкнут относительно бинарного взятия meet: если a,b ∈ S, то a ⊓ b ∈ S.

LaTeX

$$$a \in S \land b \in S \Rightarrow a \wedge b \in S$$$

Lean4

theorem infClosed : InfClosed (S : Set X) := by rintro a ha b hb; rw [← sInf_pair]; exact S.sInf_mem (pair_subset ha hb)

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

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

Разделы

Аффилиация

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