mk_le_mk — Mathlib

English

Let S and T be sublocales of a frame X. Then S ≤ T if and only if the carrier of S is contained in the carrier of T.

Русский

Пусть S и T — подлокали X. Тогда S ≤ T тогда и только тогда, когда носитель S включён в носитель T.

LaTeX

$$$S \le T \iff \operatorname{carrier}(S) \subseteq \operatorname{carrier}(T)$$$

Lean4

@[simp]
theorem mk_le_mk (carrier₁ carrier₂ : Set X) (sInf_mem'₁ sInf_mem'₂ himp_mem'₁ himp_mem'₂) :
    mk carrier₁ sInf_mem'₁ himp_mem'₁ ≤ mk carrier₂ sInf_mem'₂ himp_mem'₂ ↔ carrier₁ ⊆ carrier₂ :=
  .rfl

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