instFrameMinimalAxioms — Mathlib

English

The range of a nucleus, as a substructure, satisfies the Frame.MinimalAxioms.

Русский

Диапазон нуклеуса как подструктура удовлетворяет минимальным аксиомам рам.

LaTeX

$$$\\text{Frame.MinimalAxioms}(\\operatorname{range}(n))$$$

Lean4

instance instFrameMinimalAxioms : Frame.MinimalAxioms (range n) where
  inf_sSup_le_iSup_inf a
    s := by
    simp_rw [← Subtype.coe_le_coe, iSup_subtype', iSup, sSup, n.giAux.gc.u_inf]
    rw [rangeFactorization_coe, ← mem_range.1 a.prop, ← map_inf]
    apply n.monotone
    simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf, le_rfl]

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