subset — Mathlib

English

A subset of a cospherical set is cospherical.

Русский

Подмножество косферического множества косферично.

LaTeX

$$$$ \forall ps_1, ps_2, \ ps_1 \subseteq ps_2 \Rightarrow Cospherical(ps_2) \Rightarrow Cospherical(ps_1). $$$$

Lean4

/-- A subset of a cospherical set is cospherical. -/
theorem subset {ps₁ ps₂ : Set P} (hs : ps₁ ⊆ ps₂) (hc : Cospherical ps₂) : Cospherical ps₁ :=
  by
  rcases hc with ⟨c, r, hcr⟩
  exact ⟨c, r, fun p hp => hcr p (hs hp)⟩

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