instCanLiftSetCoeAndIsIrreducibleIsClosed

English

There exists a lifting from subsets of α to irreducible closed subsets of α, sending s to ⟨s, IsIrreducible s ∧ IsClosed s⟩ whenever s has these properties.

Русский

Существует подьём из подмножеств α в irreducible closed множества α, отображающий s в ⟨s, IsIrreducible s ∧ IsClosed s⟩, если такие свойства выполняются.

LaTeX

$$CanLift(Set α, IrreducibleCloseds α) with prf s hs := ⟨⟨s, hs.1, hs.2⟩, rfl⟩$$

Lean4

instance : CanLift (Set α) (IrreducibleCloseds α) (↑) (fun s ↦ IsIrreducible s ∧ IsClosed s) where
  prf s hs := ⟨⟨s, hs.1, hs.2⟩, rfl⟩

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