toSublocale_le_toSublocale — Mathlib

English

For nuclei m and n, the inclusion of their associated sublocales is reversed with respect to the original nucleus order: m.toSublocale ≤ n.toSublocale iff n ≤ m.

Русский

Для нуклеусов m и n включение соответствующих сублокал противоположно порядку нуклеусов: m.toSublocale ≤ n.toSublocale тогда и только тогда, когда n ≤ m.

LaTeX

$$$m^{\mathrm{toSublocale}} \le n^{\mathrm{toSublocale}} \;\iff\; n \le m$$$

Lean4

@[simp]
theorem toSublocale_le_toSublocale {m n : Nucleus X} : m.toSublocale ≤ n.toSublocale ↔ n ≤ m := by
  simp [← SetLike.coe_subset_coe]

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