Theorems · Theorem · order theory

ClosureOperator.ofCompletePred.congr_simp

∀ {α : Type u_1} [inst : CompleteLattice α] (p p_1 : α → Prop) (e_p : p = p_1)
  (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)),
  ClosureOperator.ofCompletePred p hsinf = ClosureOperator.ofCompletePred p_1 ⋯

Defined in: Mathlib.Order.SupClosed
Cited by: 0 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Quot.sound
Assumes: CompleteLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
CompleteLatticestatement and proof · cited by 1,048
InfSet.sInfstatement and proof · cited by 935
ClosureOperatorstatement · cited by 371
ClosureOperator.ofCompletePredstatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.