subtypeSubtypeEquivSubtype — Mathlib

English

If for all x, q x → p x, then { x : Subtype p // q x.1 } ≃ Subtype q.

Русский

Если для каждого x верно q x → p x, то { x : Subtype p // q x.1 } эквивалентно Subtype q.

LaTeX

$$$(\\forall x, q x \\Rightarrow p x) \\Rightarrow { x : \\text{Subtype } p // q x.1 } \\simeq \\text{Subtype } q$$$

Lean4

/-- If the outer subtype has more restrictive predicate than the inner one,
then we can drop the latter. -/
@[simps!]
def subtypeSubtypeEquivSubtype {α} {p q : α → Prop} (h : ∀ {x}, q x → p x) : { x : Subtype p // q x.1 } ≃ Subtype q :=
  (subtypeSubtypeEquivSubtypeInter p _).trans <| subtypeEquivRight fun _ => and_iff_right_of_imp h

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