Skip to content

Commit

Permalink
Fix indent
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud authored Jan 26, 2024
1 parent d4d30af commit 3ffd0fc
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Order/Filter/Ker.lean
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_k
@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp
@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := gi_principal_ker.gc.u_inf
@[simp] lemma ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⨅ i, ker (f i) :=
gi_principal_ker.gc.u_iInf
gi_principal_ker.gc.u_iInf
@[simp] lemma ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⨅ f ∈ S, ker f :=
gi_principal_ker.gc.u_sInf
gi_principal_ker.gc.u_sInf
@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := gi_principal_ker.u_l_eq _

@[simp] lemma ker_pure (a : α) : ker (pure a) = {a} := by rw [← principal_singleton, ker_principal]
Expand Down

0 comments on commit 3ffd0fc

Please sign in to comment.