toNucleus_le_toNucleus — Mathlib

English

Let S and T be sublocales of a frame X. The order on their associated nuclei is the reverse of inclusion: S.toNucleus ≤ T.toNucleus if and only if T ≤ S.

Русский

Пусть S и T — сублокалы кадра X. Порядок их связанных нуклеусов противоположен включению: S.toNucleus ≤ T.toNucleus тогда и только тогда, когда T ≤ S.

LaTeX

$$$\mathrm{toNucleus}(S) \le \mathrm{toNucleus}(T) \;\Longleftrightarrow\; T \le S$$$

Lean4

@[simp]
theorem toNucleus_le_toNucleus : S.toNucleus ≤ T.toNucleus ↔ T ≤ S := by simp [← Nucleus.range_subset_range]

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