ssubset — Mathlib

English

If N <r M, then N.E ⊂ M.E (N has a strictly smaller ground set).

Русский

Если N — строгое ограничение M, то N.E ⊂ M.E (у N строго меньше основание).

LaTeX

$$$ N <_r M \\Rightarrow N.E \\subset M.E $$$

Lean4

theorem ssubset (h : N <r M) : N.E ⊂ M.E := by
  obtain ⟨R, -, rfl⟩ := h.1
  refine h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)
  rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]

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