isBasis_iff_isBasis_closure_of_subset'

English

If I ⊆ X, then I is a basis of X if and only if I is a basis of closure(X) and X ⊆ E, where E is the ground set.

Русский

Если I ⊆ X, то I является базисом X тогда и только тогда, когда I является базисом замыкания X и X ⊆ E, где E — множество оснований.

LaTeX

$$$I \subseteq X \Rightarrow M.IsBasis I X \iff M.IsBasis I (M.closure X) \land X \subseteq M.E$$$

Lean4

theorem isBasis_iff_isBasis_closure_of_subset' (hIX : I ⊆ X) : M.IsBasis I X ↔ M.IsBasis I (M.closure X) ∧ X ⊆ M.E :=
  ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset_ground⟩, fun h ↦ h.1.isBasis_subset hIX (M.subset_closure X h.2)⟩

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